Категорная Семантика
Зависимых Типов
Если рассматривать лямбда исчисление CoC как вычислительную теорию, то ее семантика будет категория, в которой морфизмы — это преобразования (подстановки), а объекты — это всевозможные контексты. Очевидно, что такая категория не малая! Таким образом подстановка в теории типов согласно изоморфизму Карри-Говарда должна соответствовать Пулбеку категории контекстов. Да-да, это — те самые контексты Г, в которых хранятся переменные (x:A) и которые еще называются телескопами. Однако, в отличии от подстановки, которая всегда ассоциативна в тоерии типов, Пулбек может быть вообще говоря не ассоциативным, поэтому тут вручную рихтуется это несоответствие через дополнительный функтор.
Классическая модель Dybjer называлась Categories with Families, а модель Воеводского называется С-Systems и хранит контекст не как вложенные сигма, а как List с ограниченной длинной (рафинированый вектор). Но в остальном модель похожая. В нашей базовой библиотеке есть полная формализация модели Воеводского и наброски модели Дыбьера. Статьи пока нет, но черновик уже положен.
CSystem : U
= (ob : nat -> U)
* (hom : Sigma nat ob -> Sigma nat ob -> U)
* (isC : isPrecategory (Sigma nat ob, hom))
* (c0 : isC0System ob hom isC)
* isCSystem (ob, hom, isC, c0)
Definition of a universe category
uc : U
= (C : precategory)
* (_ : isCategory C)
* (pt : terminal C)
* (V : carrier C) * (VT : carrier C) * (p : hom C VT V)
* ((f : homTo C V) -> hasPullback C (V, f, VT, p))
An equivalence of universe categories is an equivalence of categories
compatible with the "p" morphism
ucEquiv (A B : uc) : U
= (e : catEquiv A.1 B.1)
* (V : Path (carrier B.1) (e.1.1 A.2.2.2.1) B.2.2.2.1)
* (VT : Path (carrier B.1) (e.1.1 A.2.2.2.2.1) B.2.2.2.2.1)
* (PathP (<i>hom B.1 (VT@i) (V@i))
(e.1.2.1 A.2.2.2.2.1 A.2.2.2.1 A.2.2.2.2.2.1) B.2.2.2.2.2.1)
[2]. https://www.youtube.com/watch?v=JsHminiPzzs
[3]. M.Sokhatskyi. Issue II: Inductive Types